Repository navigation
plan: scope the axiom + syllogism lens — argument as the fourth reachability substrate (SCOPE-ONLY) - #5521
Merged
Conversation
gunbai-bot
Bot
changed the title
briansrls
added a commit
that referenced
this pull request
Jun 22, 2026
…erived parked list - Lane 8 Ingestion (the §4 other-half, was MISSING): emit=ingest⁻¹ over one GrammarRelation; DecodeFidelity fail-closed; parser-wall is a corner. Needs owner (C10). - Lane 9 TypeScript self-host (the §7 medium-agnostic proof at scale, was a tail-bullet): emit compiler as TS + per-realization merkle fixed point. Needs owner (C11). - Parked list now DERIVED from DESIGN open-threads + parked work-items (not hand-curated — same §6 leak as the status snapshot); adds Value::Null, axiom lens (#5521), Measure migration, std §3 leaks, path-literal census, hermetic-testing. - Lane 3: re-added quick-ant's dropped audit items (workflow_dispatch dup OOM, dormant resolve cache ~191s, edge-(b) affected-set). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
SCOPE-ONLY design for the next expressibility-frontier instance: the axiom + syllogism lens (DESIGN open thread #1, ROADMAP §0). Builds nothing — adds
docs/plans/axiom-syllogism-lens.md+ its ROADMAP inbound link, for the parent review → operator build-nod.What it delivers (the four asks)
Frontier partition of syllogism-enforcement (per
docs/plans/expressibility-frontier.md):graph_has_multi_node_scc— the §4 acyclicity test turned on the argument itself), closed axiom set (no smuggled premise). Decidable graph facts; unwritable once claims are substrate nodes.The
.dagmodel —Axiom/Claim/Argumentcarriers that reusestd/graph.dag(cycle detection, DFS, adjacency) +std/logic.dag(syllogisticClassical) +std/induction.dag; the DESIGN §1–§7 chain transcribed as rows. No fork: this is theinert-layer-lens.md§8 reachability rule's fourth substrate (code · docs · lenses · argument), not a second reachability authority.First target = DESIGN.md itself (the §7 recursion) — the doc checks its own serial structure is a real consequence-chain, with discriminating RED-on-revert witnesses (delete a
becauseedge → orphan RED; add a forward edge → cycle RED; add a fourth root → smuggled-axiom RED; empty argument → non-vacuity RED).Vertical slice — three carriers + a §1-only instance + one witness file, pure
.dag, no host bridge (the argument's universe is the declared row set, so it's strictly cheaper than the doc-graph wall §0 reachability-completeness lens: doc-graph instance as first gating wall (generalize #5433, no fork); see docs/plans/inert-layer-lens.md §8 #5484). The smallest nod-able artifact that proves the wall on real claims.Open questions flagged for the nod
Row authority (transcribed vs derived-from-prose), claim granularity, the independent-peer node kind (§1 allows peers, not only consequences — the one unsettled modeling decision), and first-target order (§1-only first vs whole chain).
Honors the doc-reachability wall (#5484): new
docs/plans/X.mdships with its inbound link in the same PR.🤖 Generated with Claude Code